Try Our New BETA Version
(navigation image)
Home American Libraries | Canadian Libraries | Universal Library | Community Texts | Project Gutenberg | Children's Library | Biodiversity Heritage Library | Additional Collections
Search: Advanced Search
Anonymous User (login or join us)

View the book

item image

(~36 pg)Read Online
(1.5 M)PDF
(113.0 K)EPUB
(~36 pg)Kindle
(~36 pg)Daisy
(41.3 K)Full Text
(631.7 K)DjVu

All Files: HTTPS Torrent (2/0)

Help reading texts



Derived preconditions and their use in program synthesis (1982)

Author: Smith, Douglas R.
Subject: Automatic theorem proving
Publisher: Monterey, California : Naval Postgraduate School
Language: English
Call number: ocm80333400
Digitizing sponsor: Naval Postgraduate School, Dudley Knox Library
Book contributor: Naval Postgraduate School, Dudley Knox Library
Collection: navalpostgraduateschoollibrary; fedlink; americana

Full catalog record: MARCXML

[Open Library icon]This book has an editable web page on Open Library.



Cover title

"March 1982"--Cover

"Prepared for: Naval Postgraduate School, Monterey, California 93940."

Includes bibliographical references (p. 25-26)

Technical report; 1982

In this paper we pose and begin to explore a deductive problem more general than that of finding a proof that a given goal formula logically follows from a given set of hypotheses. The problem is most simply stated in the propositional calculus: given a goal A and hypothesis H we wish to find a formula P, called a precondition, such that A logically follows from both P and H. A precondition provides any additional conditions under which A can be shown to follow from H. A slightly more complex definition of preconditions in a first-order theory is given and used throughout the paper. A formal system based on natural deduction is presented in which preconditions can be derived. A number of examples are then given which show how derived preconditions are used in a program synthesis method we are developing. These uses include theorem proving, formula simplification, simple code generation, the completion of partial specifications for a subalgorithm, and other tasks of a deductive nature. (Author)

ck/ 4/15/09

Be the first to write a review
Downloaded 66 times

Selected metadata

Page-progression: lr
Scanningcenter: sanfrancisco
Mediatype: texts
Shiptracking: y0443
Identifier: derivedprecondit00smit
Ppi: 350
Camera: Canon EOS 5D Mark II
Operator: associate-veronica-romero@...
Scandate: 20130201181354
Republisher: associate-karina-martinez@...
Imagecount: 36
Identifier-ark: ark:/13960/t9378pp59
Ocr: ABBYY FineReader 8.0
Sponsordate: 20130228

Terms of Use (31 Dec 2014)